
def main():
    x: int = nondet_int()
    y: int = nondet_int()
    __ESBMC_assume(x > 0)
    d = y/x # 这里是否会出现除零错误？


# 调用main函数
main()
